COMMENT ⊗   VALID 00014 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00005 00002	.EVERY HEADING (Preliminary User Manual,  ,{DATE})
 00007 00003	That is, variables are represented as "subscripted x's ", and each statement
 00009 00004	.BEGIN DOUBLE SPACE
 00014 00005	Now let's try running the first example.  Assume that a disk file, EX1, has been prepared
 00018 00006	Now let's run the second example. Assume that the axiomatization is on a file named
 00023 00007	.BEGIN DOUBLE SPACE
 00027 00008	II. COMMANDS TO EXAMINE THE LIST OF CLAUSES
 00030 00009	.BEGIN DOUBLE SPACE
 00033 00010	INsert		IN <name> <statements>  IN <name> DSK: <file>
 00036 00011	III. COMMANDS FOR PERFORMING RULES OF INFERENCE
 00040 00012	IV. COMMANDS FOR SUB-PROOFS AND PROOF-CHECKING.
 00045 00013	Example 3.  A simple example of  subproof generation.
 00047 00014	When the prover is unable to make new deductions which satisfy the current
 00050 ENDMK
⊗;
.EVERY HEADING (Preliminary User Manual,  ,{DATE})

Preliminary User's Manual for the Theorem Prover

The current program is a resolution- and paramodulation-based theorem prover
with extensive facilities for on-line control.  Perhaps the easiest introduction
is to follow the development of a few examples.

.BEGIN VERBATIM
Example 1.
Consider the following set of statements:

(1)	(∀x∀y){P(x,y) ∧ P(y z) ⊃ G(x,z)}

(2)	(∀y∃x){P(x,y)}

We might interpret these statements as claiming
	"For all x and y, if x is the parent of y and y is the parent
        of z, then x is the grandparent of z,"
and
	"Everyone has a parent."
.END;


Given these statements as hypotheses we might wish to know if there were individuals, x and
 y such that x is the grandparent of y. We could pose that question as the statement:

.BEGIN VERBATIM

(3)	 (∃x∃y){G(x,y)}

.END;


It is  clear that (3) does indeed follow from (1) and (2). How do we  formulate the problem for the 
theorem prover? 

Here is one axiomatization:

.BEGIN VERBATIM

∀(x1 x2)(P(x1 x2) ∧ P(x2 x3) ⊃ G(x1 x3)); ;
∀(x2)∃(x1)P(x1 x2); ;
∃(x1 x2)G(x1 x2); ;
.END;
That is, variables are represented as "subscripted x's ", and each statement
is terminated by a semicolon.  The input statements are also expected to be
partitioned into three sets: the axioms, the hypotheses, and the theorem to be
proved. Each set of statements is also terminated by a semicolon. 

.NEXT PAGE

Example 2.

In an investigation of axiomatizations of elementary group theory the following statements
arose:

.BEGIN VERBATIM

(1)	x*x = y*y
(2)	x*(y*y) = x
(3)	x*(y*z) = z*(y*x)
(4)	x*(x*y)  = y
(5)	(x*z)*(y*z) = x*y

.END;

Question: Does (5) follow from (1)-(4)?

The answer is "yes" but it is not immediately obvious.  It is more difficult 
to establish than Example 1.
Notice that this Example is a pure equality formulation, requiring only replacements
of terms by other terms.
This example could be presented to the prover as:

.BEGIN VERBATIM

E(F(X1 X1) F(X2 X2));
E(F(X1 F(X2 X2)) X1);
E(F(X1 F(X2 X3)) F(X3 F(X2 X1)));
E(F(X1 F(X1 X2)) X2); ;
;
E(F(F(X1 X3) F(X2 X3)) F(X1 X2)); ;

.END;


Before presenting a more complicated example, we shall describe how to use the prover
on these first Examples.





.NEXT PAGE

.BEGIN DOUBLE SPACE
Once the input file has been prepared you are ready to used the theorem prover.
The command: RUN PROVER [P,JRA] , will select the current version of the program.
The appearence of an asterisk (*) signifies that the program is ready.
If you wish the program to make an initial selection of strategies  for your problem
then type: (PROVE DSK: filename). The exact strategies which are chosen are described in
a  later section.  The program will however ask whether the equality replacement
rule is to be applied.
.NARROW 8;
    (IS THERE AN EQUALITY PREDICATE (Y/ N))
.WIDEN;
If you do respond, "Y", then the program   wants to know which predicate letter
is to be interpreted as  equality.
.NARROW 8;
(WHAT IS IT)
.WIDEN;
if you would rather  select you own strategies then type: (TRY DSK: filename).
You will then be asked to respond to a series of questions  concerning  selection
of  editing and choice strategies.
.NARROW 8;
THE-FOLLOWING-CHOICE-STRATEGIES-ARE-AVAILABLE:
<list of available strategies> ;see pg.[ ] for the current  strategies and their meaning.
PICK-SOME
.WIDEN;
Unless no choice strategies are desired (signified by typing NONE) the prover
wiil ask if more are desired. If no more are desired, type N or NO.  The strategy 
used in the proof attempt will be the conjunction of the selected strategies.

In either mode of operation, TRY or PROVE, the  program begins operation as soon
as it has sufficient information from the user.
If the set of statements consisting of the axioms, hypotheses and the negation of the theorem
is found to be inconsistent, then the sequence of deductions which exhibits that
inconsistency is displayed on the console.  This refutation and the set of strategies
which were employed are also saved on a disk file . The name of the file 
is created from the name of the input file,differing only in
having the extension,  PRF.
Thus, for example, (PROVE DSK: FOO) and (PROVE DSK: (FOO.A)) would create an output
file named FOO.PRF. If the  input initially comes for the console using (PROVE) or (TRY), 
then the output file is given the  name, PRF.PRF.
It is also possible that the prover terminate without finding a refutation.
This could occur either because the selected strategies do not form a complete set
or because the initial set is not inconsistent. In either case the program types
 NO-PROOF-FOUND and enters the clause editor to wait for commands from the user.

.END;

.NEXT PAGE

Now let's try running the first example.  Assume that a disk file, EX1, has been prepared
containing the axiomatization. What follows is a running commentary on what should 
occur. Material preceeded by | is commentary; statements typed by the user are preceeded
by *.

.BEGIN VERBATIM

*RUN PROVER [P,JRA]		|retrieve the current prover.

*(PROVE DSK: EX1)		|Request that the program pick the
				|strategies while running EX1.
TYPE-AXIOMS:			|The program is accepting the axioms.
TYPE-HYPOTHESES:
TYPE-THEOREM:

HERE-ARE-THE-CLAUSES:		|What follows are the translations 
				|of the input into clause-form, with
G(X1,X2) ¬P(X3,X2) ¬P(X1 X3)	|the redundant statements removed.
P(HYP65(X1),X1)			|HYP65 is a generated Skolem function.
¬G(X1,X2)			|The translation of the negation of 
(IS THERE AN EQUALITY PREDICATE (Y / N)?) |the theorem.
*N				|There is no equality predicate.

4 ¬P(X1,X2) -P(X3 X1)		|A deduction which has been added to 
				|the list of clauses.
COUNT = 1			|There was only one resolvent formed
LEVEL = 1			|on level one.
ELAPSED-TIME = 333		|The execution time in milliseconds.

.GROUP
5 ¬P(X1 X2)

COUNT = 3
LEVEL = 2			|Three resolvents have been formed by
ELAPSED-TIME = 500		|the end of level 2. (Two have been 
				|retained.)
NIL 1 4				|A contradiction. These next six 
1 -P(X1 X2) 3 4			|lines are the refutation. I.e.:
3 ¬P(X1,X2) ¬P(X3 X1) 5 6	|  6    5
4 P(HYP65(X1), X1) HYP 1     	|   \  /
5 G(X1,X2) ¬P(X3,X2) ¬P(X1 X3) AX 1|  3     4
6 ¬G(X1,X2) THM 1		|       \  /
				|         1    4
				|          \  /
				|            NIL


.APART
.END;
.GROUP
Notes: 
.NARROW 8;
1. Each clause -- deduction or translation of input -- is  a disjunction of the
literals which appear.  For example, ¬P(X1,X2) ¬P(X3,X1), represents
¬P(X1,X2) ∨ ¬P(X3,X1).

2. The partition of the input into the three sets is reflected in the description of the
refutation tree. That is, P(HYP65(X1),X1) resulted from the translation of one of the
hypotheses;  ¬G(X1,X2) came from the negation of the theorem.

3. A copy of the refutation tree, relevant statistics, and  a description of the
actual strategies used, now appears on a file named EX1.PRF.

.WIDEN
.APART
.NEXT PAGE

Now let's run the second example. Assume that the axiomatization is on a file named
 EX2.

.BEGIN VERBATIM 

*RUN PROVER [P,JRA]

*(PROVE DSK: EX2)		|Again, let the program
				|pick the strategies.
TYPE-AXIOMS
TYPE-HYPOTHESES
TYPE-THEOREM

HERE-ARE-THE-CLAUSES:

E(F(X1,X1),F(X2,X2))
E(F(X1,F(X2,X2)),X1)
E(F(X1,F(X2,X3)),F(X3,F(X2,X1)))
E(F(X1,F(X1,X2)),X1)
¬E(F(F(THM66,THM68),F(THM67,THM68)),F(THM66,THM67))
				|Again, THMn's are generated
				|Skolem constants.
(IS THERE AN EQUALITY PREDICATE (Y/N)?)
*Y				|This time there is.
(WHAT IS IT ?)
*E				|E is obviously  it.

NIL 1 2				|An immediate contradiction
1 E(X1,X1)			|We know E is reflexive
2 ¬E(F(THM66,THM67),F(THM66,THM67)) 3 4 |moderate mystery.
3 E(F(X1,F(X2,X3)),F(X3,F(X2,X1))) AX 3
4 ¬E(F(F(THM66,THM68),F(THM67,THM68)),F(THM66,THM67)) THM 1
.END;

Notes:



1. The `refutation' is a bit mysterious.  A more sympathetic proof recovery
mechanism is contemplated, but perhaps some of the current mystery can be dispelled.

A `natural' proof might be:

.BEGIN VERBATIM
	1.  (x*z)*(y*z) = z*(y*(x*z))  replacement using (3)
	2.  z*(y*(x*z)) = z*(z*(x*y))  replacement using (3)
	3.  z*(z*(x*y)) = x*y          replacement using (4)
.END;

The above proof is indeed a translation of the machine proof.  Besides replacement,
the prover also has a special rule of simplification. Whenever an equality
formulation is presented to the prover, a list ,SL,is made consisting
 of all the equalities which occur in the input.
In the current example, SL would consist of everything but the negation of the 
theorem. Let  t1 = t2 be a member of SL. Whenever a deduction is formed  (but before
it has been added to the memory of the prover) we attempt to match t1 against terms
occurring in the deduction. If matches can be made we repalce those terms with the
appropriate instance of t2. It is this simplified deduction which is presented to the
prover.

.GROUP

Thus the refutation really is:
.BEGIN VERBATIM

¬E(F(F(THM66,THM68),F(THM67,THM68)),F(THM66,THM67)) THM 1
	\
	  \
	    \  E(F(X1,F(X2,X3)),F(X3,F(X2,X1))) AX 3
	      \      /
		\  /
¬E(F(THM68,F(THM67,F(THM66,THM68))),F(THM66,THM67)) 
		\                      by replacement
	  	  \
		    \ E(F(X1,F(X2,X3)),F(X3,F(X2,X1))) AX 3
		      \       /
			\   /
¬E(F(THM68,F(THM68,F(THM66,THM67))),F(THM66,THM67))
		\		       by simplification
		  \
		    \ E(F(X1,F(X1,X2)),X2) AX 4
		      \       /
			\   /
         ¬E(F(THM66,THM67),F(THM66,THM67))
 	       \ 		       by simplification
		 \
		   \       E(X1,X1)
		     \        /
		       \    /
			NIL
				by resolution
.END;
.APART


.NEXT PAGE

.BEGIN DOUBLE SPACE
Most applications of the prover lie in that gray area between a quick proof and the occurrence of 
NO-PROOF.  That is, an application of the prover usually generated a large number
of deductions before either a proof is found or no more deductions can be made
under the current strategy settings.
It is this area which can be profitably explored using interactive commands.
If the user sees a deduction which  should lead to the desired  refutation
he is able to guide the program to the explicit contradiction.  If he sees
a deduction which he feels is interesting, he can explore its consequences in the
set of statements.  If he feels that the strategy settings are ill-chosen
then he can abort the current proof-search and pick new strategies.  The next
sections give detailed descriptions of the current on-line commands.

.END;
I. GENERAL BOOKEEPING COMMANDS.

CHange		CH;
.NARROW 16;
It is  frequently desireable to change some of the strategies while a proof attempt is in progress.
CHange initiates a  dialogue with the user describing what choice and editing strategies
are currently active and asking which are to be changed.
.WIDEN;

CUrrent		CU;
.NARROW 16;
This command simply lists the current strategy settings.
.WIDEN;

DSkout		DS <filename>;
.NARROW 16;
This command diverts future output to specified disk file. 
.WIDEN;

EVal	 	EV;
.NARROW 16;
This command is  mostly a debugging aid and is included for completeness.  The casual users should not have to resort
to its use.  EVal enters a READ-EVAL-PRINT. To return to the editor, type @END.
.WIDEN;

HAlt		HA;
.NARROW 16;
HAlt stops the prover is such a state that if the current core image is saved, it can
be continued.  To  resume execution of such a core image, type RUN  DSK: name.  When the
asterisk appears you are in the on-line editor. Then type TErminate.
.WIDEN;

End Of file	EO;
.NARROW 16;
EOf is used to terminate the DSkout command.

.WIDEN;
HElp		HE;
.NARROW 16;
This command will type a list of the available editing commands along with an abbreviated description of their action.
.WIDEN;

TErminate 	TE;
.NARROW 16;
This command is used to terminate the editing process and return to the prover.
.WIDEN;






.NEXT PAGE

II. COMMANDS TO EXAMINE THE LIST OF CLAUSES
.BEGIN DOUBLE SPACE

Each  clause which has been retained by the prover -- axiom, hypothesis, negation of the 
theorem or deduction -- is given a numbe, the first axiom, the
number 1., etc.. These numbers are permanently assigned, even though certain
actions of the prover may remove  clauses from consideration by the rules of inference.
Clauses which have been so deleted are displayed as *DE*.  When the editor is entered,
a hypothetical pointer is initialized to the first clause.  This first  set of commands
allow the used to manipulate the set of clauses using the associated numbers.

.END;

FLoat UP	FU; or FL UP;
.NARROW 16 ;
Moves the pointer up through the list of clauses.  The motion is stopped
either by striking a key or by reaching the upper extreme of the
list. FLoat UP may also be apbbreviated as FU.
.WIDEN;

FLoat DOwn	FD; or FL DO;
.NARROW 16;
The counterpart of FLoat UP. FLoat Down may also be abbreviated 
as FD.
.WIDEN;

UP		UP n;
.NARROW 16;
UP is to be followed by an integer, N.  The effect of this command
is to move the pointer up N clauses from its current  setting. As the pointer
is moved, the interviening clauses are printed.
If N = 0, then the pointer is immediately moved to the beginning of the 
clause list.  As with the FLoat commands,striking a key will stop the pointer.
.WIDEN;

DOwn		DO n;
.NARROW 16;
The counterpart of UP. DOwn 0 moves the pointer to the end of
the list.
.WIDEN;

GO		GO n;
.NARROW 16;
GO is to be followed by an integer designating a clauses.  The pointer goes  
immediately to the designated clause.
.WIDEN;

.NEXT PAGE

.BEGIN DOUBLE SPACE
Though these commands  have proved quite useful, experience  has shown that more
global manipulation of the clauses is needed. Therefore we have commands for
assigning names to subsets of the clause list, and commands for manipulating these sets.
Just as each element of the primary list of clauses is assigned a unique positive integer,
so is each element of each named subset.  For example to refer to the second element of the
set  named FOO, use (FOO 2); to refer to the second and third elements, use (FOO 2 3).
Certain commands, like REsolve or PAramodualte create new names, like RES1,RES2, etc.
or PAR1, PAR2. These created names are local to that call on the on-line editor.
Names which were initiated by the user using the SEt command are global.

The following BNF equations will be used in the sequel:
 
.END;
.BEGIN VERBATIM;
<clauses> := <ind> 

	  := <clauses><ind>

<ind> := <integer>   ;select the designated clause in the clauselist.

      := <name>        ;select the designated set of clauses

      := (<name> <soi>);select the designated clauses from <name>

<name>:= <identifier>  ;

<soi> := <integer>

      := <soi>,<integer>

.END;
CLear		CL <name>;	
.NARROW 16;
CLear takes a name as argument. This command only removes the
name from the symbol table; it does not affect the clauses attached to the
name.
.WIDEN;

Delete		DE <clauses>;
.NARROW 16;
The designated clauses are deleted from the memory of the prover. Attempts to display
 such clauses will print *DE*.  Other attempts to use deleted clauses in editing commands
will  invoke an error message.
.WIDEN;

DIsplay		DI <clauses>;
.NARROW 16;
This command displays all the elements of <clauses>;_
.WIDEN;

INsert		IN <name> <statements>;  IN <name> DSK: <file>;
.NARROW 16;
This command is used to enter new clauses into the  clause editor.
The first argument to INsert is a <name>. What follows is a set of clauses, or a file designator.
If the clauses are typed they must conform to the standard input format; if a file
designator is given, the specified file must be in the correct format.
.WIDEN;

MErge		ME <clauses>; <clauses>;
.NARROW 16;
This commnad deletes all clauses from the first set whichare subsumed by elements of the second set.
.WIDEN;

SAve		SA <clauses>;
.NARROW 16;
Most of the results of the  on-line commands: deductions, insertions, substitutions,etc,
are local to the clause editor. To include any of these resulting clauses in the memory of the prover
use the Save command.
.WIDEN;


SEt		SE <name> <clauses>;
.NARROW 16;
SEt <name> <clauses>; has the effect of assigning
to <name>, the sequence of clauses selected by the <clauses>.
Within a particular proof attempt, the names selected by the user are retained.
.WIDEN;

SUbstitute	SU <term1> FOR <term2> IN <clauses>;
.NARROW 16;
This command is used to form substitution instances of selected clauses. These created instances
are attached to the name, ASSERT. The original clauses are not affected.
.WIDEN;
.NEXT PAGE
.BEGIN DOUBLE SPACE

The commands listed above give us a reasonably powerful set of instructions for
manipulating the clause list. Clearly, before we can really begin to guide the prover
we must be able to perform the rules of inference on-line. The next  set of commands
begins to do this.


.END;



III. COMMANDS FOR PERFORMING RULES OF INFERENCE



PAramodulate		PA <clauses>; <clauses>;
.NARROW 16;
This command(which cries for abbreviation) is the counterpart  to REsolve.
All equality literals of the form t1=t2, are used in equality replacements in the following manner:
let s be any term, not a variable, which occurs in some literal in one of the clauses.
If s occurs no deeper than PDEPTH (see the appendix for PDEPTH) and there is a substitution
 unifying s and t1, then the occurrence of t1 is replaced by the appropriate instantiation
of t2.
.WIDEN;

REsolve			RE <clauses>;<clauses>;
.NARROW 16;
This command takes a pair of <clauses> as arguments.  The resolvents of these
two sets are formed, a unique name is generated and the resolvents are assigned to that
new name.  The generated names are presently of the form RESn, for some integer,n.
.WIDEN;

SImplify		SImplify <clauses>; BY <clauses>;
.NARROW 16;
This command is similar to the PA command.  Here the second set of clauses is to be a
list of equality units, again of the form t1=t2. Terms occuring in the first set of clauses
which unify with elements, t1, are replaced by instances of t2.  DDEPTH determines the
depth to which the match is attempted.
.WIDEN;

Example 3.  A simple example of the use of the rules of inference.

Assume that R is the equality predicate and that we have just struck a key on the
console.

.BEGIN VERBATIM


*DI 1,2,3;			|Display the first three clauses
1 R(D(X1,X2),O) ¬LE(X1,X2)
2 ¬R(D(U,D(A,B)),U)
3 LE(O,X1)

*PA 1; 2;			|Use replacement on 1 and 2.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME: PAR1	|PAR1 is a created name.

1 ¬R(U,O) ¬LE(U,D(A,B))

*PA 2; 3;			|Try to use the replacement rule
NO-PARAMODULANTS		|on clauses 2, and 3.

*RE 1; 3;
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:RES1	|RES1 is another created
				|name.
1 R(D(O,X1),O)

*PA RES1; RES1;			|Created names are legal.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:PAR2	|PAR2 is a new name.

1 R(O,O)			|True.

*SA (PAR1 1);			|Add this deduction to the memory
				|of the prover;

.END;

.NEXT PAGE


IV. COMMANDS FOR SUB-PROOFS AND PROOF-CHECKING.

.BEGIN DOUBLE SPACE
Though the commands, REsolve and PAramodulate, are useful for fine control of the
prover, is is often useful to demand larger inference steps. That is, using some of the
existing clauses in memory, with perhaps some additional assumptions, we wish the
prover to attempt to establish the validity of a  first order formula. While this
subproof is  under investigation the state of the main proof should be preserved.
The commands in this section are used to initiate and control such subproofs.

.END;


ABort		AB ; or AB <clauses>;

.NARROW 16;
This command is used to manually abort a proof attempt, returning to the previous
level.  If <clauses> is present, then the selected clauses are returned and assigned
to a created name.
.WIDEN;


ASsume		AS <statements>; or AS DSK: <file>;
.NARROW 16;
This command introduces the  designated statements to the prover.  The statements are
assigned to a local name, ASSUMPTIONS, and will appear as hypotheses under the name HYPS in the forthcomming
subproof.
.WIDEN;


USing		US <clauses>;
.NARROW 16;
The selected clauses in the prover's memory are designated to be the AXIOMS in the
subproof.
.WIDEN;

PRove		PR <statement>; or PR DSK: <file>;
.NARROW 16;
The <statement> is translated and will be attached to the name LEMMA. The negation 
of the statement is also formed and will be used in the subproof. Thus both the positive and negative 
tanslates are formed.  The positive translate is maintained for the convenience of the
user since after the lemma has been established  it  should be available for further 
deductions.  Within the subproof the negation of the <statement> will appear under the local
name, THMS.
.WIDEN;

These three commands,--ASsume, USing, and PRove -- are used to initialize the call
on the prover.  Either ASsume or USing may be omitted. There are two  commands to
commence the subproof.

EXecute		EX;
.NARROW 16;
EXecute begins the subproof using a computed set of stategies.
.WIDEN;

TRy		TR;
.NARROW 16;
TRy first enters the strategy selection dialog, then begins the subproof with the chosen strategies.
.WIDEN;

In both cases the strategies of the subproof are completely local.  They in no way
affect the strategies in the parent proof. If a key is struck while in the subproof
the editor is entered and can manipulate the local clauselist or initiate another
subproof. The TErminate command will comtinue the subproof, the ABort command will
return to the previous level.


.NEXT PAGE

Example 3.  A simple example of  subproof generation.

Suppose that we have struck a key during a proof-search.
.BEGIN VERBATIM

*AN 10;				|Display the ancestry of 
P(A) 1 2			|clause no. 10.
1 P(A) P(B)  AX 1
2 ¬P(B)	     HYP 1

*ASSUME P(B) ∨ ¬P(A); ;		|Setup the assumptions for the
				|lemma.
*USING 10;			|Use clause no. 10 in the attempt

*PROVE P(B);;

*EX;				|This initiates the subproof.

NIL 1 2
1 P(A) AX 1			|Clause 10 becomes an axiom
2 ¬P(A)	3 4			|with the subproof.
3 P(B) ¬P(A) HYP 1
4 ¬P(B) THM 1			|The negation of the lemma

CONTRADICTION-FOUND-FOR-LEMMA
				|We are now back in the  editor
*DI 10;				|Display clause no. 10.
P(A)

*DI LEMMA;			|The translate of the statement 
P(B)				|to be PROVEed.

*USING LEMMA;

*PROVE ∃(X1)P(X1);;		|LEMMA now becomes the translate
*EX;				|this clause.
NIL 1 2
1 P(B) AX 1
2 ¬P(X1) THM 1

CONTRADICTION-FOUND-FOR-LEMMA

*DI LEMMA;			|ED1 is a ubiquitous Skolem 
P(ED1)				|constant.
.END;

.NEXT PAGE


V. COMMANDS USEFUL WHEN NO PROOF IS FOUND

.BEGIN DOUBLE SPACE

When the prover is unable to make new deductions which satisfy the current
strategies it will report that no refutation can be found, and will enter
the on-line editor. At this time  the user can examine the list of clauses,
perform rules of inference, initiate sub-proofs, or use the other on-line commands.
The user also has the opportunity to save any or all of the current deductions
and begin a the proof search again, perhaps with new strategies.
The user can also force a proof attempt to be abandoned by typing AB;.  This
has exactly the same effect as if the prover could make no new deductions.

.END;

ABandon		AB;

.NARROW 16
AB, typed in this context (not in a subproof) terminates the main proof attempt,
enters the on-line editor, and waits for commands.
.WIDEN

TErminate	TE <clauses>; or TE;

.NARROW 16
If <clauses> are present then they are added to the list of clauses named THMS.
The list, AXIOMS, HYPS, and THMS are preserved and a new proof attempt is begun.
If the initial attempt was through PROVE then the user is asked if he still wants
automatic strategy selection.  If the initial attempt was through TRY or the
user does not wish automatic selection, then a dialogue is begun describing the
current strategies and asking if changes are desired.
Then a new proof search is begun.
.WIDEN

.BEGIN DOUBLE SPACE

This use of AB and TE is useful for feeding `interesting' deductions back into a
proof search without having to restart the whole process.  The derivation tree
of any such saved derived clause is maintained for the proof recovery mechanisms
but such clauses appear to be `input' clauses to the rules of inference.

.END;